//初始强制复位
initial assume(!rst_n);
// 复位后初始值检查
always @(posedge wclk) begin
    if ($past(!rst_n)) begin // 复位释放后的第一个周期
        assert(wr_ptr == 5'b00000);
    end
end
// 复位后初始值检查
always @(posedge rclk) begin
    if ($past(!rst_n)) begin // 复位释放后的第一个周期
        assert(rd_ptr == 5'b00000);
    end
end
// 复位稳定时写指针自增正常 ps：考虑循环自增
always @(posedge wclk) begin
    if ($past(rst_n,3) && $past(rst_n,2) && $past(rst_n) && rst_n && $past(wr_en) && wr_en && $past(!full) && !full) begin // 复位释放后的第一个周期
        assert(wr_ptr == ($past(wr_ptr)+1)%32);
    end
end
// 满时禁止写入
always @(posedge wclk) begin
    if ( rst_n && $past(rst_n) && $past(full) && full) begin
        assert($stable(wr_ptr));
    end
end

// 非写操作时存储不变
generate for (genvar i = 0; i < 16; i++) begin : mem_stability
    always @(posedge wclk) begin
        if ( $past(rst_n) && rst_n &&!($past(wr_en) || $past(!full)) && !(wr_en || !full)) begin
            assert($stable(mem[i]));  // 检查每个存储单元
        end
    end
end
endgenerate

// 复位中断写操作
always @(posedge wclk) begin
    if ($fell(rst_n)) begin
        assert(!wr_ptr);
    end
end

always @(posedge wclk) begin
    cover (full);
    cover (empty);
end